Using the verification prototype, we generated a \begin{changebar}USE
specification and a search configuration as shown in
Fig.~\ref{fig:toolchain}.\end{changebar} After adding the constraints (Table
\ref{tab:OCLConsts}) to the USE specification, we ran the USE tool once for each
constraint.

Out of the 18 constraints defined in Table \ref{tab:OCLConsts}, two
multiplicity invariants were found to be violated by the transformation:
$\mathtt{CompositionType\_component}$ and $\mathtt{SwcToEcuMapping\_component}$.
In other words, our transformation can generate a \emph{CompositionType} with no
\emph{ComponentPrototype}s and/or a \emph{SwcToEcuMapping} with no
\emph{ComponentPrototype}s. Both of these possible outputs violate the
multiplicities defined in the AUTOSAR metamodel (Fig. \ref{fig:systempfig}).
The counterexamples were found by \begin{changebar}USE even within a scope of
just one object per concrete class.\end{changebar}

Due to the page limit, we only show an excerpt of the counterexample generated
for the invariant $\mathtt{CompositionType\_component}$ in Fig. \ref{fig:ctrex}. The
counterexample shows that the rule $\mathtt{initSysTemp}$ maps a \emph{PhysicalNode}
to five elements, one of which is \emph{CompositionType}. Since the rule does
not have any restrictions on the generated \emph{CompositionType}, it was
created without associating it to any \emph{ComponentPrototype} through the
\emph{component} association.
The counterexample for the $\mathtt{SwcToEcuMapping\_component}$ invariant was
similar showing that the $\mathtt{initSingleSwc2EcuMapping}$ rule creates a
\emph{SwcToEcuMapping} element without mandating that it is associated to any
\emph{SwCompToEcuMapping\_component} element through the \emph{component}
association.
\begin{figure*}[tb]
\centering
 %\resizebox{1\textwidth}{3.5cm}{%{0.8\textwidth}{!} %2.4cm
  \includegraphics[scale=0.40]{imgs/ctrex.jpg}\\[-2ex]
 %}
\caption{Counterexample generated for the mult. inv. $\mathtt{CompositionType\_component}$.}
\label{fig:ctrex}
%\vspace{-0.6cm}
\end{figure*}

After examining the two counterexamples generated by USE for the two
violated multiplicity invariants, we identified two bugs in two rules shown in
Table~\ref{tab:buggyRules}:
$\mathtt{initSysTemp}$ and $\mathtt{initSingleSwc2EcuMapping}$. The bold,
underlined text are the updates to the rules that fix the two
bugs. $\mathtt{initSysTemp}$ initially mapped a \emph{PhysicalNode} to many
elements, including a \emph{CompositionType} that must contain at least one
\emph{ComponentPrototype}. If the \emph{PhysicalNode} did not have any
\emph{Module} in any of its \emph{Partition}s, then the created
\emph{CompositionType} will not contain any \emph{ComponentPrototype}s. Thus we
added a matching constraint to the \emph{PhysicalNode} matched by the rule to
ensure that any of its \emph{Partition}s must contain at least one
\emph{Module}. Similarly, $\mathtt{initSingleSwc2EcuMapping}$ initially mapped a
\emph{Partition} to a \emph{SwcToEcuMapping} that must contain at least one
\emph{SwCompToEcuMapping\_component}. If the \emph{Partition} did not have any
\emph{Module}, then the created \emph{SwcToEcuMapping} will not contain any
\emph{SwCompToEcuMapping\_component}. Thus we added a matching constraint to the
\emph{Partition} matched by the rule to ensure that it must contain at least one
\emph{Module}.
% \begin{figure*}[tbh]
%  \resizebox{0.8\textwidth}{2.0cm}{%{0.8\textwidth}{!} %2.4cm
%   \includegraphics{imgs/buggyRules.jpg}
%  }
% \caption{The two transformation rules that required changes to address
% violations in multiplicity invariants.}
% \label{fig:buggyRules}
% \vspace{-0.6cm}
% \end{figure*}
\begin{table}[tb]%tbh
%\vspace{-0.6cm}
 	\centering
 	\scriptsize%\tiny%\scriptsize%\footnotesize
 	\renewcommand{\arraystretch}{1} %was 2.4, 1.5
\begin{tabular}{|p{12.2cm}|}
\hline
rule initSysTemp\{ \\
from  ph: GM!PhysicalNode
{\underline{{\bf{(ph.partition$\mathtt{\to}$exists(p$\mathtt{\mid}$p.Module$\mathtt{\to}$notEmpty()))}}}} \\
to \\
  \hspace*{5ex} \ldots \\
	\hspace*{5ex} compostype:autosar!CompositionType( \\ 
	\hspace*{5ex} \ldots \\
  \hspace*{5ex} component $\mathtt{\gets}$%
           ph.partition$\mathtt{\to}$collect(p$\mathtt{\mid}$%
           p.Module)$\mathtt{\to}$flatten()$\mathtt{\to}$collect(m$\mathtt{\mid}$ \\
  \hspace*{5ex} thisModule.resolveTemp(m, 'comp'))) \}
\\ \hline
rule initSingleSwc2EcuMapping \{ \\
from p:GM!Partition%
((GM!PhysicalNode.allInstances()$\mathtt{\to}$one(ph$\mathtt{\mid}$%
ph.partition$\mathtt{\to}$includes(p))) \\
	\hspace*{5ex} {\underline{{\bf{and(p.module$\mathtt{\to}$notEmpty()))}}}} \\ 
to \\
	\hspace*{5ex} mapping:autosar!SwcToEcuMapping ( \\           
  \hspace*{5ex} shortName  $\mathtt{\gets}$ p.Name, \\ 
  \hspace*{5ex} component $\mathtt{\gets}$ p.Module%
           $\mathtt{\to}$collect(m$\mathtt{\mid}$thisModule.resolveTemp(m, 'mapComp')),\\           
	\hspace*{5ex} ecuInstance $\mathtt{\gets}$%
           thisModule.resolveTemp((GM!PhysicalNode.allInstances()$\mathtt{\to}$%
           select(ph$\mathtt{\mid}$ \\
  \hspace*{5ex} ph.partition$\mathtt{\to}$includes(p)))$\mathtt{\to}$first(),'EcuInst'))\}
           \\ \hline 
 \end{tabular}
\caption{The two rules that required updates to address the two violations of
multiplicity invariants.}
\label{tab:buggyRules}
%\vspace{-1cm}
\end{table} 

The 18 constraints were reverified on the updated
transformation, and were all found to be satisfied.